$\forall$$A$, $B$:Type, $R$:($A$$\rightarrow$$A$$\rightarrow\mathbb{P}$), $S$:($B$$\rightarrow$$B$$\rightarrow\mathbb{P}$), $f$:($A$$\rightarrow$$B$).
\\[0ex]RelsIso($A$;$B$;$x$,$y$.$R$($x$,$y$);$x$,$y$.$S$($x$,$y$);$f$) $\Rightarrow$ Sym($B$;$x$,$y$.$S$($x$,$y$)) $\Rightarrow$ Sym($A$;$x$,$y$.$R$($x$,$y$))